\begin{tabbing}
$\forall$$i$:Id, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, ${\it snd}_{1}$, ${\it snd}_{2}$:${\it kl}$:Knd$\times$IdLnk fp$\rightarrow$ (Id$\times$Top) List.
\\[0ex]${\it snd}_{1}$ $\parallel$ ${\it snd}_{2}$
\\[0ex]$\Rightarrow$ (\=msg{-}spec{-}loc{-}decl(${\it snd}_{1}$ $\oplus$ ${\it snd}_{2}$;$i$;${\it da}$)\+
\\[0ex]$\Leftrightarrow$
\\[0ex]msg{-}spec{-}loc{-}decl(${\it snd}_{1}$;$i$;${\it da}$) \& msg{-}spec{-}loc{-}decl(${\it snd}_{2}$;$i$;${\it da}$))
\-
\end{tabbing}